$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $L$:$T$ List, $i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$.
\\[0ex]no\_repeats($T$;$L$) $\Rightarrow$ mu($\lambda$${\it i@}_{0}$.eqof(${\it eq}$)($L$[$i$],$L$[${\it i@}_{0}$])) $=$ $i$ $\in$ $\mathbb{Z}$